Change the representation of reachability claims, part 1 #2007
Conversation
ana-pantilie
changed the title
|
|
||
| instance | ||
| InternalVariable variable | ||
| => From (Map (SomeVariable variable) (TermLike variable)) (Conditional variable ()) |
There was a problem hiding this comment.
Why not From (Substitution variable) (Conditional variable ())? Or at least, there should be a direct instance.
| where | ||
| from = | ||
| from @(Predicate variable) @(Conditional variable ()) | ||
| . from @(Substitution variable) @(Predicate variable) |
There was a problem hiding this comment.
Shouldn't we put the Substitution into the substitution field? This would unpack the substitution into the predicate, right?
There was a problem hiding this comment.
Yes, this isn't right. Thanks for spotting this!
kore/src/Kore/Internal/TermLike.hs
Outdated
| -> Binder (SetVariable variable) (TermLike variable) | ||
| refreshSetBinder = refreshBinder refreshSetVariable | ||
|
|
||
| type Modality = Sort -> Alias (TermLike VariableName) |
There was a problem hiding this comment.
I would prefer to make this a sum type and do the conversion to Alias entirely in applyModality.
kore/src/Kore/Step/ClaimPattern.hs
Outdated
| claimPattern left rightTerm = | ||
| ClaimPattern | ||
| { left | ||
| , right = OrPattern.parseFromTermLike rightTerm |
There was a problem hiding this comment.
I don't like converting between TermLike and OrPattern. This will go away once the series of pull requests is merged, right?
There was a problem hiding this comment.
I gave this a little more thought, and maybe we won't actually need to parse the RHS in any other places except when actually parsing the definition. I'll remove it now.
| instance Diff AllPathRule | ||
|
|
||
| instance Unparse AllPathRule where | ||
| unparse claimPattern' = |
There was a problem hiding this comment.
I think it would be a good idea to unparse through SentenceClaim.
There was a problem hiding this comment.
I actually found this very strange when copying the instance from RulePattern. I thought claims should unparse to their pattern form. Adding the claim {} declaration at the beginning would make this a sentence.
|
|
||
| import Prelude.Kore | ||
|
|
||
|
|
|
|
||
| newtype Pair variable = Pair (TermLike variable, Predicate variable) | ||
|
|
||
| class RuleBase base rule where |
There was a problem hiding this comment.
Is this class very useful, now that we can have whole Patterns on the left- and right-hand sides?
There was a problem hiding this comment.
The tests in Simplify should work on RewriteRules as well. I might remove this class once I clean up all the old code, but right now it seemed the cleanest way to run the tests with old/new claims and rewrite rules.
3 participants
Part of #1278
Reviewer checklist
stack test --coveragestack haddock